M:MsgA, k:Knd, s:M.state, v:M.da(k), x:Id, w:(M.ds(x)). M.ef(k,x,s,v)?w  M.ds(x) 

latex

Definitions

MsgA, M.state, M.da(a), M.ds(x), M.ef(k,x,s,v)?w, Unit, x  dom(f), b, A, f(x), t.1, product-deq(A;B;a;b), Valtype(da;k), IdLnk, KindDeq, x(s), T, atom2-deq-aux, suptype(S; T), P  Q, eq_atom$n(x;y), P  Q, f(a), EqDecider(T), t.2, <a, b>, P & Q, case b of inl(x) => s(x) | inr(y) => t(y), True, b, Atom$n, if b then t else f fi , State(ds), Knd, left + right, x:A.B(x), a:A fp B(a), x,y:A//B(x;y), x,y. t(x;y), P  Q, , qeq(r;s), tt, EquivRel(T;x,y.E(x;y)), s = t, , A  B, x:A  B(x), , , , S  T, x:AB(x), x. t(x), x.A(x), Top, f(x)?z, Void, Type, x:A. B(x), Id, IdDeq, t  T

Lemmas

id-deq wf, Id wf, fpf-cap-void-subtype, fpf-cap wf, rationals wf, int nzero wf, b-union wf, btrue wf, qeq wf2, bool wf, quotient wf, deq wf, subtype rel self, assert wf, iff wf, eq atom wf2, rev implies wf, atom2-deq-aux, fpf wf, true wf, squash wf, top wf, Knd wf, pi2 wf, Kind-deq wf, IdLnk wf, product-deq wf, pi1 wf, ma-valtype wf, ma-state wf, fpf-ap wf, not wf, bnot wf, fpf-trivial-subtype-top, fpf-dom wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, msga wf